0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 86 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 0 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 19 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 AND
↳9 PiDP
↳10 UsableRulesProof (⇔, 0 ms)
↳11 PiDP
↳12 PiDPToQDPProof (⇒, 0 ms)
↳13 QDP
↳14 QDPSizeChangeProof (⇔, 0 ms)
↳15 YES
↳16 PiDP
↳17 UsableRulesProof (⇔, 0 ms)
↳18 PiDP
↳19 PiDPToQDPProof (⇒, 0 ms)
↳20 QDP
↳21 UsableRulesReductionPairsProof (⇔, 179 ms)
↳22 QDP
↳23 MRRProof (⇔, 0 ms)
↳24 QDP
↳25 PisEmptyProof (⇔, 0 ms)
↳26 YES
lessleavesC_in_gg(nil, cons(T5, T6)) → lessleavesC_out_gg(nil, cons(T5, T6))
lessleavesC_in_gg(cons(nil, T19), cons(T13, T14)) → U5_gg(T19, T13, T14, pB_in_ggag(T13, T14, X18, T19))
pB_in_ggag(T13, T14, X18, T19) → U2_ggag(T13, T14, X18, T19, appendA_in_gga(T13, T14, X18))
appendA_in_gga(nil, T29, T29) → appendA_out_gga(nil, T29, T29)
appendA_in_gga(cons(T36, T37), T38, cons(T36, X47)) → U1_gga(T36, T37, T38, X47, appendA_in_gga(T37, T38, X47))
U1_gga(T36, T37, T38, X47, appendA_out_gga(T37, T38, X47)) → appendA_out_gga(cons(T36, T37), T38, cons(T36, X47))
U2_ggag(T13, T14, X18, T19, appendA_out_gga(T13, T14, X18)) → pB_out_ggag(T13, T14, X18, T19)
pB_in_ggag(T13, T14, T22, T19) → U3_ggag(T13, T14, T22, T19, appendA_in_gga(T13, T14, T22))
U3_ggag(T13, T14, T22, T19, appendA_out_gga(T13, T14, T22)) → U4_ggag(T13, T14, T22, T19, lessleavesC_in_gg(T19, T22))
lessleavesC_in_gg(cons(cons(T51, T52), T53), cons(T13, T14)) → U6_gg(T51, T52, T53, T13, T14, appendA_in_gga(T52, T53, X68))
U6_gg(T51, T52, T53, T13, T14, appendA_out_gga(T52, T53, X68)) → lessleavesC_out_gg(cons(cons(T51, T52), T53), cons(T13, T14))
lessleavesC_in_gg(cons(cons(T51, T52), T53), cons(T13, T14)) → U7_gg(T51, T52, T53, T13, T14, appendA_in_gga(T52, T53, T56))
U7_gg(T51, T52, T53, T13, T14, appendA_out_gga(T52, T53, T56)) → U8_gg(T51, T52, T53, T13, T14, pB_in_ggag(T13, T14, X18, cons(T51, T56)))
U8_gg(T51, T52, T53, T13, T14, pB_out_ggag(T13, T14, X18, cons(T51, T56))) → lessleavesC_out_gg(cons(cons(T51, T52), T53), cons(T13, T14))
U4_ggag(T13, T14, T22, T19, lessleavesC_out_gg(T19, T22)) → pB_out_ggag(T13, T14, T22, T19)
U5_gg(T19, T13, T14, pB_out_ggag(T13, T14, X18, T19)) → lessleavesC_out_gg(cons(nil, T19), cons(T13, T14))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
lessleavesC_in_gg(nil, cons(T5, T6)) → lessleavesC_out_gg(nil, cons(T5, T6))
lessleavesC_in_gg(cons(nil, T19), cons(T13, T14)) → U5_gg(T19, T13, T14, pB_in_ggag(T13, T14, X18, T19))
pB_in_ggag(T13, T14, X18, T19) → U2_ggag(T13, T14, X18, T19, appendA_in_gga(T13, T14, X18))
appendA_in_gga(nil, T29, T29) → appendA_out_gga(nil, T29, T29)
appendA_in_gga(cons(T36, T37), T38, cons(T36, X47)) → U1_gga(T36, T37, T38, X47, appendA_in_gga(T37, T38, X47))
U1_gga(T36, T37, T38, X47, appendA_out_gga(T37, T38, X47)) → appendA_out_gga(cons(T36, T37), T38, cons(T36, X47))
U2_ggag(T13, T14, X18, T19, appendA_out_gga(T13, T14, X18)) → pB_out_ggag(T13, T14, X18, T19)
pB_in_ggag(T13, T14, T22, T19) → U3_ggag(T13, T14, T22, T19, appendA_in_gga(T13, T14, T22))
U3_ggag(T13, T14, T22, T19, appendA_out_gga(T13, T14, T22)) → U4_ggag(T13, T14, T22, T19, lessleavesC_in_gg(T19, T22))
lessleavesC_in_gg(cons(cons(T51, T52), T53), cons(T13, T14)) → U6_gg(T51, T52, T53, T13, T14, appendA_in_gga(T52, T53, X68))
U6_gg(T51, T52, T53, T13, T14, appendA_out_gga(T52, T53, X68)) → lessleavesC_out_gg(cons(cons(T51, T52), T53), cons(T13, T14))
lessleavesC_in_gg(cons(cons(T51, T52), T53), cons(T13, T14)) → U7_gg(T51, T52, T53, T13, T14, appendA_in_gga(T52, T53, T56))
U7_gg(T51, T52, T53, T13, T14, appendA_out_gga(T52, T53, T56)) → U8_gg(T51, T52, T53, T13, T14, pB_in_ggag(T13, T14, X18, cons(T51, T56)))
U8_gg(T51, T52, T53, T13, T14, pB_out_ggag(T13, T14, X18, cons(T51, T56))) → lessleavesC_out_gg(cons(cons(T51, T52), T53), cons(T13, T14))
U4_ggag(T13, T14, T22, T19, lessleavesC_out_gg(T19, T22)) → pB_out_ggag(T13, T14, T22, T19)
U5_gg(T19, T13, T14, pB_out_ggag(T13, T14, X18, T19)) → lessleavesC_out_gg(cons(nil, T19), cons(T13, T14))
LESSLEAVESC_IN_GG(cons(nil, T19), cons(T13, T14)) → U5_GG(T19, T13, T14, pB_in_ggag(T13, T14, X18, T19))
LESSLEAVESC_IN_GG(cons(nil, T19), cons(T13, T14)) → PB_IN_GGAG(T13, T14, X18, T19)
PB_IN_GGAG(T13, T14, X18, T19) → U2_GGAG(T13, T14, X18, T19, appendA_in_gga(T13, T14, X18))
PB_IN_GGAG(T13, T14, X18, T19) → APPENDA_IN_GGA(T13, T14, X18)
APPENDA_IN_GGA(cons(T36, T37), T38, cons(T36, X47)) → U1_GGA(T36, T37, T38, X47, appendA_in_gga(T37, T38, X47))
APPENDA_IN_GGA(cons(T36, T37), T38, cons(T36, X47)) → APPENDA_IN_GGA(T37, T38, X47)
PB_IN_GGAG(T13, T14, T22, T19) → U3_GGAG(T13, T14, T22, T19, appendA_in_gga(T13, T14, T22))
U3_GGAG(T13, T14, T22, T19, appendA_out_gga(T13, T14, T22)) → U4_GGAG(T13, T14, T22, T19, lessleavesC_in_gg(T19, T22))
U3_GGAG(T13, T14, T22, T19, appendA_out_gga(T13, T14, T22)) → LESSLEAVESC_IN_GG(T19, T22)
LESSLEAVESC_IN_GG(cons(cons(T51, T52), T53), cons(T13, T14)) → U6_GG(T51, T52, T53, T13, T14, appendA_in_gga(T52, T53, X68))
LESSLEAVESC_IN_GG(cons(cons(T51, T52), T53), cons(T13, T14)) → APPENDA_IN_GGA(T52, T53, X68)
LESSLEAVESC_IN_GG(cons(cons(T51, T52), T53), cons(T13, T14)) → U7_GG(T51, T52, T53, T13, T14, appendA_in_gga(T52, T53, T56))
U7_GG(T51, T52, T53, T13, T14, appendA_out_gga(T52, T53, T56)) → U8_GG(T51, T52, T53, T13, T14, pB_in_ggag(T13, T14, X18, cons(T51, T56)))
U7_GG(T51, T52, T53, T13, T14, appendA_out_gga(T52, T53, T56)) → PB_IN_GGAG(T13, T14, X18, cons(T51, T56))
lessleavesC_in_gg(nil, cons(T5, T6)) → lessleavesC_out_gg(nil, cons(T5, T6))
lessleavesC_in_gg(cons(nil, T19), cons(T13, T14)) → U5_gg(T19, T13, T14, pB_in_ggag(T13, T14, X18, T19))
pB_in_ggag(T13, T14, X18, T19) → U2_ggag(T13, T14, X18, T19, appendA_in_gga(T13, T14, X18))
appendA_in_gga(nil, T29, T29) → appendA_out_gga(nil, T29, T29)
appendA_in_gga(cons(T36, T37), T38, cons(T36, X47)) → U1_gga(T36, T37, T38, X47, appendA_in_gga(T37, T38, X47))
U1_gga(T36, T37, T38, X47, appendA_out_gga(T37, T38, X47)) → appendA_out_gga(cons(T36, T37), T38, cons(T36, X47))
U2_ggag(T13, T14, X18, T19, appendA_out_gga(T13, T14, X18)) → pB_out_ggag(T13, T14, X18, T19)
pB_in_ggag(T13, T14, T22, T19) → U3_ggag(T13, T14, T22, T19, appendA_in_gga(T13, T14, T22))
U3_ggag(T13, T14, T22, T19, appendA_out_gga(T13, T14, T22)) → U4_ggag(T13, T14, T22, T19, lessleavesC_in_gg(T19, T22))
lessleavesC_in_gg(cons(cons(T51, T52), T53), cons(T13, T14)) → U6_gg(T51, T52, T53, T13, T14, appendA_in_gga(T52, T53, X68))
U6_gg(T51, T52, T53, T13, T14, appendA_out_gga(T52, T53, X68)) → lessleavesC_out_gg(cons(cons(T51, T52), T53), cons(T13, T14))
lessleavesC_in_gg(cons(cons(T51, T52), T53), cons(T13, T14)) → U7_gg(T51, T52, T53, T13, T14, appendA_in_gga(T52, T53, T56))
U7_gg(T51, T52, T53, T13, T14, appendA_out_gga(T52, T53, T56)) → U8_gg(T51, T52, T53, T13, T14, pB_in_ggag(T13, T14, X18, cons(T51, T56)))
U8_gg(T51, T52, T53, T13, T14, pB_out_ggag(T13, T14, X18, cons(T51, T56))) → lessleavesC_out_gg(cons(cons(T51, T52), T53), cons(T13, T14))
U4_ggag(T13, T14, T22, T19, lessleavesC_out_gg(T19, T22)) → pB_out_ggag(T13, T14, T22, T19)
U5_gg(T19, T13, T14, pB_out_ggag(T13, T14, X18, T19)) → lessleavesC_out_gg(cons(nil, T19), cons(T13, T14))
LESSLEAVESC_IN_GG(cons(nil, T19), cons(T13, T14)) → U5_GG(T19, T13, T14, pB_in_ggag(T13, T14, X18, T19))
LESSLEAVESC_IN_GG(cons(nil, T19), cons(T13, T14)) → PB_IN_GGAG(T13, T14, X18, T19)
PB_IN_GGAG(T13, T14, X18, T19) → U2_GGAG(T13, T14, X18, T19, appendA_in_gga(T13, T14, X18))
PB_IN_GGAG(T13, T14, X18, T19) → APPENDA_IN_GGA(T13, T14, X18)
APPENDA_IN_GGA(cons(T36, T37), T38, cons(T36, X47)) → U1_GGA(T36, T37, T38, X47, appendA_in_gga(T37, T38, X47))
APPENDA_IN_GGA(cons(T36, T37), T38, cons(T36, X47)) → APPENDA_IN_GGA(T37, T38, X47)
PB_IN_GGAG(T13, T14, T22, T19) → U3_GGAG(T13, T14, T22, T19, appendA_in_gga(T13, T14, T22))
U3_GGAG(T13, T14, T22, T19, appendA_out_gga(T13, T14, T22)) → U4_GGAG(T13, T14, T22, T19, lessleavesC_in_gg(T19, T22))
U3_GGAG(T13, T14, T22, T19, appendA_out_gga(T13, T14, T22)) → LESSLEAVESC_IN_GG(T19, T22)
LESSLEAVESC_IN_GG(cons(cons(T51, T52), T53), cons(T13, T14)) → U6_GG(T51, T52, T53, T13, T14, appendA_in_gga(T52, T53, X68))
LESSLEAVESC_IN_GG(cons(cons(T51, T52), T53), cons(T13, T14)) → APPENDA_IN_GGA(T52, T53, X68)
LESSLEAVESC_IN_GG(cons(cons(T51, T52), T53), cons(T13, T14)) → U7_GG(T51, T52, T53, T13, T14, appendA_in_gga(T52, T53, T56))
U7_GG(T51, T52, T53, T13, T14, appendA_out_gga(T52, T53, T56)) → U8_GG(T51, T52, T53, T13, T14, pB_in_ggag(T13, T14, X18, cons(T51, T56)))
U7_GG(T51, T52, T53, T13, T14, appendA_out_gga(T52, T53, T56)) → PB_IN_GGAG(T13, T14, X18, cons(T51, T56))
lessleavesC_in_gg(nil, cons(T5, T6)) → lessleavesC_out_gg(nil, cons(T5, T6))
lessleavesC_in_gg(cons(nil, T19), cons(T13, T14)) → U5_gg(T19, T13, T14, pB_in_ggag(T13, T14, X18, T19))
pB_in_ggag(T13, T14, X18, T19) → U2_ggag(T13, T14, X18, T19, appendA_in_gga(T13, T14, X18))
appendA_in_gga(nil, T29, T29) → appendA_out_gga(nil, T29, T29)
appendA_in_gga(cons(T36, T37), T38, cons(T36, X47)) → U1_gga(T36, T37, T38, X47, appendA_in_gga(T37, T38, X47))
U1_gga(T36, T37, T38, X47, appendA_out_gga(T37, T38, X47)) → appendA_out_gga(cons(T36, T37), T38, cons(T36, X47))
U2_ggag(T13, T14, X18, T19, appendA_out_gga(T13, T14, X18)) → pB_out_ggag(T13, T14, X18, T19)
pB_in_ggag(T13, T14, T22, T19) → U3_ggag(T13, T14, T22, T19, appendA_in_gga(T13, T14, T22))
U3_ggag(T13, T14, T22, T19, appendA_out_gga(T13, T14, T22)) → U4_ggag(T13, T14, T22, T19, lessleavesC_in_gg(T19, T22))
lessleavesC_in_gg(cons(cons(T51, T52), T53), cons(T13, T14)) → U6_gg(T51, T52, T53, T13, T14, appendA_in_gga(T52, T53, X68))
U6_gg(T51, T52, T53, T13, T14, appendA_out_gga(T52, T53, X68)) → lessleavesC_out_gg(cons(cons(T51, T52), T53), cons(T13, T14))
lessleavesC_in_gg(cons(cons(T51, T52), T53), cons(T13, T14)) → U7_gg(T51, T52, T53, T13, T14, appendA_in_gga(T52, T53, T56))
U7_gg(T51, T52, T53, T13, T14, appendA_out_gga(T52, T53, T56)) → U8_gg(T51, T52, T53, T13, T14, pB_in_ggag(T13, T14, X18, cons(T51, T56)))
U8_gg(T51, T52, T53, T13, T14, pB_out_ggag(T13, T14, X18, cons(T51, T56))) → lessleavesC_out_gg(cons(cons(T51, T52), T53), cons(T13, T14))
U4_ggag(T13, T14, T22, T19, lessleavesC_out_gg(T19, T22)) → pB_out_ggag(T13, T14, T22, T19)
U5_gg(T19, T13, T14, pB_out_ggag(T13, T14, X18, T19)) → lessleavesC_out_gg(cons(nil, T19), cons(T13, T14))
APPENDA_IN_GGA(cons(T36, T37), T38, cons(T36, X47)) → APPENDA_IN_GGA(T37, T38, X47)
lessleavesC_in_gg(nil, cons(T5, T6)) → lessleavesC_out_gg(nil, cons(T5, T6))
lessleavesC_in_gg(cons(nil, T19), cons(T13, T14)) → U5_gg(T19, T13, T14, pB_in_ggag(T13, T14, X18, T19))
pB_in_ggag(T13, T14, X18, T19) → U2_ggag(T13, T14, X18, T19, appendA_in_gga(T13, T14, X18))
appendA_in_gga(nil, T29, T29) → appendA_out_gga(nil, T29, T29)
appendA_in_gga(cons(T36, T37), T38, cons(T36, X47)) → U1_gga(T36, T37, T38, X47, appendA_in_gga(T37, T38, X47))
U1_gga(T36, T37, T38, X47, appendA_out_gga(T37, T38, X47)) → appendA_out_gga(cons(T36, T37), T38, cons(T36, X47))
U2_ggag(T13, T14, X18, T19, appendA_out_gga(T13, T14, X18)) → pB_out_ggag(T13, T14, X18, T19)
pB_in_ggag(T13, T14, T22, T19) → U3_ggag(T13, T14, T22, T19, appendA_in_gga(T13, T14, T22))
U3_ggag(T13, T14, T22, T19, appendA_out_gga(T13, T14, T22)) → U4_ggag(T13, T14, T22, T19, lessleavesC_in_gg(T19, T22))
lessleavesC_in_gg(cons(cons(T51, T52), T53), cons(T13, T14)) → U6_gg(T51, T52, T53, T13, T14, appendA_in_gga(T52, T53, X68))
U6_gg(T51, T52, T53, T13, T14, appendA_out_gga(T52, T53, X68)) → lessleavesC_out_gg(cons(cons(T51, T52), T53), cons(T13, T14))
lessleavesC_in_gg(cons(cons(T51, T52), T53), cons(T13, T14)) → U7_gg(T51, T52, T53, T13, T14, appendA_in_gga(T52, T53, T56))
U7_gg(T51, T52, T53, T13, T14, appendA_out_gga(T52, T53, T56)) → U8_gg(T51, T52, T53, T13, T14, pB_in_ggag(T13, T14, X18, cons(T51, T56)))
U8_gg(T51, T52, T53, T13, T14, pB_out_ggag(T13, T14, X18, cons(T51, T56))) → lessleavesC_out_gg(cons(cons(T51, T52), T53), cons(T13, T14))
U4_ggag(T13, T14, T22, T19, lessleavesC_out_gg(T19, T22)) → pB_out_ggag(T13, T14, T22, T19)
U5_gg(T19, T13, T14, pB_out_ggag(T13, T14, X18, T19)) → lessleavesC_out_gg(cons(nil, T19), cons(T13, T14))
APPENDA_IN_GGA(cons(T36, T37), T38, cons(T36, X47)) → APPENDA_IN_GGA(T37, T38, X47)
APPENDA_IN_GGA(cons(T36, T37), T38) → APPENDA_IN_GGA(T37, T38)
From the DPs we obtained the following set of size-change graphs:
LESSLEAVESC_IN_GG(cons(nil, T19), cons(T13, T14)) → PB_IN_GGAG(T13, T14, X18, T19)
PB_IN_GGAG(T13, T14, T22, T19) → U3_GGAG(T13, T14, T22, T19, appendA_in_gga(T13, T14, T22))
U3_GGAG(T13, T14, T22, T19, appendA_out_gga(T13, T14, T22)) → LESSLEAVESC_IN_GG(T19, T22)
LESSLEAVESC_IN_GG(cons(cons(T51, T52), T53), cons(T13, T14)) → U7_GG(T51, T52, T53, T13, T14, appendA_in_gga(T52, T53, T56))
U7_GG(T51, T52, T53, T13, T14, appendA_out_gga(T52, T53, T56)) → PB_IN_GGAG(T13, T14, X18, cons(T51, T56))
lessleavesC_in_gg(nil, cons(T5, T6)) → lessleavesC_out_gg(nil, cons(T5, T6))
lessleavesC_in_gg(cons(nil, T19), cons(T13, T14)) → U5_gg(T19, T13, T14, pB_in_ggag(T13, T14, X18, T19))
pB_in_ggag(T13, T14, X18, T19) → U2_ggag(T13, T14, X18, T19, appendA_in_gga(T13, T14, X18))
appendA_in_gga(nil, T29, T29) → appendA_out_gga(nil, T29, T29)
appendA_in_gga(cons(T36, T37), T38, cons(T36, X47)) → U1_gga(T36, T37, T38, X47, appendA_in_gga(T37, T38, X47))
U1_gga(T36, T37, T38, X47, appendA_out_gga(T37, T38, X47)) → appendA_out_gga(cons(T36, T37), T38, cons(T36, X47))
U2_ggag(T13, T14, X18, T19, appendA_out_gga(T13, T14, X18)) → pB_out_ggag(T13, T14, X18, T19)
pB_in_ggag(T13, T14, T22, T19) → U3_ggag(T13, T14, T22, T19, appendA_in_gga(T13, T14, T22))
U3_ggag(T13, T14, T22, T19, appendA_out_gga(T13, T14, T22)) → U4_ggag(T13, T14, T22, T19, lessleavesC_in_gg(T19, T22))
lessleavesC_in_gg(cons(cons(T51, T52), T53), cons(T13, T14)) → U6_gg(T51, T52, T53, T13, T14, appendA_in_gga(T52, T53, X68))
U6_gg(T51, T52, T53, T13, T14, appendA_out_gga(T52, T53, X68)) → lessleavesC_out_gg(cons(cons(T51, T52), T53), cons(T13, T14))
lessleavesC_in_gg(cons(cons(T51, T52), T53), cons(T13, T14)) → U7_gg(T51, T52, T53, T13, T14, appendA_in_gga(T52, T53, T56))
U7_gg(T51, T52, T53, T13, T14, appendA_out_gga(T52, T53, T56)) → U8_gg(T51, T52, T53, T13, T14, pB_in_ggag(T13, T14, X18, cons(T51, T56)))
U8_gg(T51, T52, T53, T13, T14, pB_out_ggag(T13, T14, X18, cons(T51, T56))) → lessleavesC_out_gg(cons(cons(T51, T52), T53), cons(T13, T14))
U4_ggag(T13, T14, T22, T19, lessleavesC_out_gg(T19, T22)) → pB_out_ggag(T13, T14, T22, T19)
U5_gg(T19, T13, T14, pB_out_ggag(T13, T14, X18, T19)) → lessleavesC_out_gg(cons(nil, T19), cons(T13, T14))
LESSLEAVESC_IN_GG(cons(nil, T19), cons(T13, T14)) → PB_IN_GGAG(T13, T14, X18, T19)
PB_IN_GGAG(T13, T14, T22, T19) → U3_GGAG(T13, T14, T22, T19, appendA_in_gga(T13, T14, T22))
U3_GGAG(T13, T14, T22, T19, appendA_out_gga(T13, T14, T22)) → LESSLEAVESC_IN_GG(T19, T22)
LESSLEAVESC_IN_GG(cons(cons(T51, T52), T53), cons(T13, T14)) → U7_GG(T51, T52, T53, T13, T14, appendA_in_gga(T52, T53, T56))
U7_GG(T51, T52, T53, T13, T14, appendA_out_gga(T52, T53, T56)) → PB_IN_GGAG(T13, T14, X18, cons(T51, T56))
appendA_in_gga(nil, T29, T29) → appendA_out_gga(nil, T29, T29)
appendA_in_gga(cons(T36, T37), T38, cons(T36, X47)) → U1_gga(T36, T37, T38, X47, appendA_in_gga(T37, T38, X47))
U1_gga(T36, T37, T38, X47, appendA_out_gga(T37, T38, X47)) → appendA_out_gga(cons(T36, T37), T38, cons(T36, X47))
LESSLEAVESC_IN_GG(cons(nil, T19), cons(T13, T14)) → PB_IN_GGAG(T13, T14, T19)
PB_IN_GGAG(T13, T14, T19) → U3_GGAG(T19, appendA_in_gga(T13, T14))
U3_GGAG(T19, appendA_out_gga(T22)) → LESSLEAVESC_IN_GG(T19, T22)
LESSLEAVESC_IN_GG(cons(cons(T51, T52), T53), cons(T13, T14)) → U7_GG(T51, T13, T14, appendA_in_gga(T52, T53))
U7_GG(T51, T13, T14, appendA_out_gga(T56)) → PB_IN_GGAG(T13, T14, cons(T51, T56))
appendA_in_gga(nil, T29) → appendA_out_gga(T29)
appendA_in_gga(cons(T36, T37), T38) → U1_gga(T36, appendA_in_gga(T37, T38))
U1_gga(T36, appendA_out_gga(X47)) → appendA_out_gga(cons(T36, X47))
appendA_in_gga(x0, x1)
U1_gga(x0, x1)
The following rules are removed from R:
LESSLEAVESC_IN_GG(cons(nil, T19), cons(T13, T14)) → PB_IN_GGAG(T13, T14, T19)
Used ordering: POLO with Polynomial interpretation [POLO]:
appendA_in_gga(nil, T29) → appendA_out_gga(T29)
POL(LESSLEAVESC_IN_GG(x1, x2)) = x1 + x2
POL(PB_IN_GGAG(x1, x2, x3)) = x1 + x2 + x3
POL(U1_gga(x1, x2)) = x1 + x2
POL(U3_GGAG(x1, x2)) = x1 + x2
POL(U7_GG(x1, x2, x3, x4)) = x1 + x2 + x3 + x4
POL(appendA_in_gga(x1, x2)) = x1 + x2
POL(appendA_out_gga(x1)) = x1
POL(cons(x1, x2)) = x1 + x2
POL(nil) = 0
PB_IN_GGAG(T13, T14, T19) → U3_GGAG(T19, appendA_in_gga(T13, T14))
U3_GGAG(T19, appendA_out_gga(T22)) → LESSLEAVESC_IN_GG(T19, T22)
LESSLEAVESC_IN_GG(cons(cons(T51, T52), T53), cons(T13, T14)) → U7_GG(T51, T13, T14, appendA_in_gga(T52, T53))
U7_GG(T51, T13, T14, appendA_out_gga(T56)) → PB_IN_GGAG(T13, T14, cons(T51, T56))
appendA_in_gga(cons(T36, T37), T38) → U1_gga(T36, appendA_in_gga(T37, T38))
U1_gga(T36, appendA_out_gga(X47)) → appendA_out_gga(cons(T36, X47))
appendA_in_gga(x0, x1)
U1_gga(x0, x1)
PB_IN_GGAG(T13, T14, T19) → U3_GGAG(T19, appendA_in_gga(T13, T14))
U3_GGAG(T19, appendA_out_gga(T22)) → LESSLEAVESC_IN_GG(T19, T22)
LESSLEAVESC_IN_GG(cons(cons(T51, T52), T53), cons(T13, T14)) → U7_GG(T51, T13, T14, appendA_in_gga(T52, T53))
U7_GG(T51, T13, T14, appendA_out_gga(T56)) → PB_IN_GGAG(T13, T14, cons(T51, T56))
appendA_in_gga(cons(T36, T37), T38) → U1_gga(T36, appendA_in_gga(T37, T38))
U1_gga(T36, appendA_out_gga(X47)) → appendA_out_gga(cons(T36, X47))
appendAingga2 > cons2 > U7GG4 > PBINGGAG3 > U3GGAG2 > LESSLEAVESCINGG2 > U1gga2 > appendAoutgga1
appendA_out_gga_1=1
cons_2=0
U1_gga_2=0
PB_IN_GGAG_3=1
U3_GGAG_2=1
appendA_in_gga_2=0
LESSLEAVESC_IN_GG_2=2
U7_GG_4=0
appendA_in_gga(x0, x1)
U1_gga(x0, x1)